Nuprl Definition : iseg
11,40
postcript
pdf
iseg(
T
;
l1
;
l2
) ==
l
:
T
List. (
l2
= append(
l1
;
l
))
latex
clarification:
iseg(
T
;
l1
;
l2
) ==
l
:
T
List. (
l2
= append(
l1
;
l
)
(
T
List))
latex
Definitions
x
:
A
.
B
(
x
)
,
s
=
t
,
type
List
,
append(
as
;
bs
)
FDL editor aliases
iseg
origin
l:T List. (l2 = append(l1; l))
l:T List. (l2 = append(l1; l) 
(T List)) l:T List. (l2 = append(l1; l))
l:T List. (l2 = append(l1; l) (T List)) x:A. B(x)